/**
 * Copyright (c) 2010 CWI Amsterdam and others. All rights reserved.
 * This program and the accompanying materials are made available
 * under the terms of the Eclipse Public License v1.0
 * which accompanies this distribution, and is available at
 * http://www.eclipse.org/legal/epl-v10.html
 * 
 * Contributors:
 *    CWI Amsterdam - initial API and implementation
 */
package nl.cwi.arne.mcrl2.toolchains;

import java.io.File;
import java.text.MessageFormat;
import java.text.ParseException;
import java.util.StringTokenizer;

import nl.cwi.arne.mcrl2.Specification;
import nl.cwi.arne.mcrl2.util.Command;
import nl.cwi.arne.mcrl2.util.MCRL2Commands;
import nl.cwi.arne.mcrl2.util.MCRL2Options;

/**
 * @author Christian Krause
 * @generated NOT
 */
public class GenerateLTSToolChain extends GenerateLPSToolChain {
	
	// Serial ID:
	private static final long serialVersionUID = 1L;
	
	// Involved files:
	private File ltsFile1, ltsFile2;
	
	// ltsinfo command:
	private Command ltsinfoCommand;
	
	// LTS info:
	private String ltsFormat = null;	
	private int numberOfStates = -1;
	private int numberOfLabels = -1;
	private int numberOfTransitions = -1;
	private boolean deterministic = false;
	
	/**
	 * Constructor.
	 * @param specification mCRL2 specification.
	 */
	public GenerateLTSToolChain(Specification specification, MCRL2Options options) {
		super(specification, options);
		initToolChain(options);
	}
	
	/**
	 * Alternative constructor.
	 */
	public GenerateLTSToolChain(File lpsFile, MCRL2Options options) {
		super(lpsFile);
		initToolChain(options);
	}

	protected GenerateLTSToolChain(String name) {
		super(name);
	}

	/*
	 * Initialize the tool chain.
	 */
	private void initToolChain(MCRL2Options options) {

		setName("Generating labeled transition system...");
		setWaitForLast(true);
		
		// We need to make sure that the LPS file is set.
		if (getLPSFile()!=null) {
			ltsFile1 = new File(getBaseFileName() + ".aut");
			ltsFile2 = options.getLtsconvert() ? new File(getBaseFileName() + "min.aut") : ltsFile1;
			
			add(MCRL2Commands.lps2lts(getLPSFile(), ltsFile1));
			if (options.getLtsconvert()) {
				add(MCRL2Commands.ltsconvert(ltsFile1, ltsFile2, options.getEquivalence()));
			}
			if (options.getLtsinfo()) {
				add(ltsinfoCommand = MCRL2Commands.ltsinfo(ltsFile2));
				setCaptureOutput(true);  // Must capture the output.
			}
			
		}
		
	}
	
	/*
	 * (non-Javadoc)
	 * @see nl.cwi.arne.mcrl2.util.ToolChain#commandFinished(nl.cwi.arne.mcrl2.util.Command)
	 */
	@Override
	protected void commandFinished(Command command) {
		super.commandFinished(command);
		if (command==ltsinfoCommand) {
			try {
				StringTokenizer lines = new StringTokenizer(ltsinfoCommand.getOutput(), CR);
				ltsFormat = (String) new MessageFormat("LTS format: {0}").parse(lines.nextToken())[0];
				numberOfStates = ((Long) new MessageFormat("Number of states: {0,number,integer}").parse(lines.nextToken())[0]).intValue();
				numberOfLabels = ((Long) new MessageFormat("Number of labels: {0,number,integer}").parse(lines.nextToken())[0]).intValue();
				numberOfTransitions = ((Long) new MessageFormat("Number of transitions: {0,number,integer}").parse(lines.nextToken())[0]).intValue();
				while (lines.hasMoreElements()) {
					String next = lines.nextToken();
					if (next.startsWith("LTS is deterministic")) deterministic = true;
					if (next.startsWith("LTS is not deterministic")) deterministic = false;
				}
			}
			catch (ParseException e) {
				e.printStackTrace();
				command.setExitCode(UNEXPECTED_OUTPUT_EXIT_CODE);
			}
		}
	}
	
	/*
	 * (non-Javadoc)
	 * @see nl.cwi.arne.mcrl2.util.ToolChain#doCleanup()
	 */
	@Override
	protected void doCleanup() {
		super.doCleanup();
		if (ltsFile1!=null && ltsFile2!=null && !ltsFile1.equals(ltsFile2)) {
			ltsFile1.delete();
		}
	}
	
	public File getLTSFile() {
		return ltsFile2;
	}
	
	protected void setLTSFile(File ltsFile) {
		this.ltsFile2 = ltsFile;
	}

	// ----- LTS info ------ //
	
	public String getLtsFormat() {
		return ltsFormat;
	}

	public int getNumberOfStates() {
		return numberOfStates;
	}

	public int getNumberOfLabels() {
		return numberOfLabels;
	}

	public int getNumberOfTransitions() {
		return numberOfTransitions;
	}

	public boolean isDeterministic() {
		return deterministic;
	}
	
}
